(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-highlight-add-annotations 'nil '(2 8 (keyword) t) '(9 10 (symbol) t) '(11 16 (keyword) t) '(18 24 (keyword) t) '(27 28 (symbol) t) '(34 39 (keyword) t) '(42 47 (keyword) t) '(50 51 (symbol) t) '(59 60 (symbol) t) '(67 73 (keyword) t) '(76 77 (symbol) t) '(79 80 (symbol) t) '(82 83 (symbol) t) '(84 89 (keyword) t) '(92 96 (keyword) t) '(105 106 (symbol) t) '(112 113 (symbol) t))
(agda2-highlight-add-annotations 'nil '(2 8 (keyword) t) '(9 10 (module) nil nil ("Issue3010.agda" . 1)) '(11 16 (keyword) t) '(25 26 (record) nil nil ("Issue3010.agda" . 25)) '(29 33 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(48 49 (field) nil nil ("Issue3010.agda" . 48)) '(52 55 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(57 58 (function) nil nil ("Issue3010.agda" . 57)) '(61 65 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(74 75 (module) nil nil ("Issue3010.agda" . 74)) '(77 78 (bound) nil nil ("Issue3010.agda" . 77)) '(81 82 (record) nil nil ("Issue3010.agda" . 25)) '(97 98 (module) nil nil ("Issue3010.agda" . 25)) '(99 100 (bound) nil nil ("Issue3010.agda" . 77)) '(103 104 (function) nil nil ("Issue3010.agda" . 103)) '(107 108 () nil nil ("Issue3010.agda" . 48)) '(110 111 (function) nil nil ("Issue3010.agda" . 57)) '(114 115 (record) nil nil ("Issue3010.agda" . 25)))
(agda2-highlight-add-annotations 'nil '(25 26 (record) nil nil ("Issue3010.agda" . 25)) '(27 28 (symbol) t) '(29 33 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)))
(agda2-highlight-add-annotations 'nil '(18 24 (keyword) t) '(25 26 (record) nil nil ("Issue3010.agda" . 25)) '(34 39 (keyword) t) '(42 47 (keyword) t) '(48 49 (field) nil nil ("Issue3010.agda" . 48)) '(50 51 (symbol) t) '(52 55 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)))
(agda2-highlight-add-annotations 'nil '(57 58 (function) nil nil ("Issue3010.agda" . 57)) '(61 65 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)))
(agda2-highlight-add-annotations 'nil '(67 73 (keyword) t) '(74 75 (module) nil nil ("Issue3010.agda" . 74)) '(76 77 (symbol) t) '(77 78 (bound) nil nil ("Issue3010.agda" . 77)) '(79 80 (symbol) t) '(81 82 (record) nil nil ("Issue3010.agda" . 25)) '(82 83 (symbol) t) '(84 89 (keyword) t) '(92 96 (keyword) t) '(105 106 (symbol) t))
(agda2-highlight-add-annotations 'nil '(97 98 (module) nil nil ("Issue3010.agda" . 25)) '(99 100 (bound) nil nil ("Issue3010.agda" . 77)))
(agda2-highlight-add-annotations 'nil '(103 104 (function) nil nil ("Issue3010.agda" . 103)))
(agda2-highlight-add-annotations 'nil '(103 104 (function) nil nil ("Issue3010.agda" . 103)) '(107 108 (field) nil nil ("Issue3010.agda" . 48)))
(agda2-highlight-add-annotations 'nil '(57 58 (function) nil nil ("Issue3010.agda" . 57)) '(110 111 (function) nil nil ("Issue3010.agda" . 57)) '(112 113 (symbol) t) '(114 115 (record) nil nil ("Issue3010.agda" . 25)))
(agda2-highlight-add-annotations 'nil '(2 8 (keyword) t) '(9 10 (module) nil nil ("Issue3010.agda" . 1)) '(11 16 (keyword) t))
(agda2-highlight-add-annotations 'nil '(59 60 (symbol) t))
(agda2-status-action "Checked")
(agda2-info-action "*All Done*" "" nil)
((last . 1) . (agda2-goals-action '()))
